add support for cmo extension #137
Closed
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
jrtc27
reviewed
Dec 18, 2021
OK, I'll try to seperate the three extensions. |
|
Thanks for an incredibly quick and thorough review.
But, at one point you say there shouldn't be random spaces, but the
guidelines said you can add them to align things vertically to make them
easier to understand.
Which would be fine if in this case he added a couple more extra spaces to
make the expressions actually line up.
Do I have that correct?
…On Fri, Dec 17, 2021 at 10:20 PM Jessica Clarke ***@***.***> wrote:
***@***.**** commented on this pull request.
Various initial feedback; generally only commented on the first instance
of something even when it applies multiple times, so please check for other
instances of things I've said, especially when it comes to code formatting
------------------------------
In Makefile
<#137 (comment)>:
> @@ -29,6 +29,7 @@ SAIL_DEFAULT_INST += riscv_insts_zbc.sail
SAIL_DEFAULT_INST += riscv_insts_zbs.sail
SAIL_DEFAULT_INST += riscv_insts_zkn.sail
SAIL_DEFAULT_INST += riscv_insts_zks.sail
+SAIL_DEFAULT_INST += riscv_insts_cmoext.sail
As you can see from the big block above, each Zfoo gets its own zfoo.sail
file, so Zicbom, Zicbop and Zicboz should get their own files named
accordingly
------------------------------
In c_emulator/riscv_platform_impl.c
<#137 (comment)>:
> @@ -20,6 +20,8 @@ uint64_t rv_ram_size = UINT64_C(0x4000000);
uint64_t rv_rom_base = UINT64_C(0x1000);
uint64_t rv_rom_size = UINT64_C(0x100);
+uint64_t rv_cache_block_size = UINT64_C(0x10);
16 bytes is a strange default, 64 seems like a more common cache line size
to default to
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> @@ -0,0 +1,245 @@
+/* ****************************************************************** */
+/* This file specifies the instructions in the cmo extension */
Not an extension name
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> @@ -0,0 +1,245 @@
+/* ****************************************************************** */
+/* This file specifies the instructions in the cmo extension */
+
+
+/* ****************************************************************** */
+union clause ast = RISCV_CBO : (cbop, regidx)
Should be specific to Zcbop
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> @@ -0,0 +1,245 @@
+/* ****************************************************************** */
+/* This file specifies the instructions in the cmo extension */
+
+
+/* ****************************************************************** */
+union clause ast = RISCV_CBO : (cbop, regidx)
+
+mapping encdec_cbop : cbop <-> bits(12) = {
+ CBO_CLEAN <-> 0b000000000001,
+ CBO_FLUSH <-> 0b000000000010,
+ CBO_INVAL <-> 0b000000000000,
+ CBO_ZERO <-> 0b000000000100
CBO_ZERO is part of a separate extension to the other three so should get
its own ast clause
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> @@ -0,0 +1,245 @@
+/* ****************************************************************** */
+/* This file specifies the instructions in the cmo extension */
+
+
+/* ****************************************************************** */
+union clause ast = RISCV_CBO : (cbop, regidx)
+
+mapping encdec_cbop : cbop <-> bits(12) = {
+ CBO_CLEAN <-> 0b000000000001,
+ CBO_FLUSH <-> 0b000000000010,
+ CBO_INVAL <-> 0b000000000000,
+ CBO_ZERO <-> 0b000000000100
+}
+
+mapping clause encdec = RISCV_CBO(cbop, rs1)
These need guards on the extensions being enabled
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> + CBO_CLEAN <-> "cbo.clean",
+ CBO_FLUSH <-> "cbo.flush",
+ CBO_INVAL <-> "cbo.inval",
+ CBO_ZERO <-> "cbo.zero"
+}
+
+mapping clause assembly = RISCV_CBO(cbop, rs1)
+ <-> cbo_mnemonic(cbop) ^ spc() ^ reg_name(rs1)
+
+val write_zero: (xlenbits, xlenbits) -> MemoryOpResult(bool) effect {wmv, wmvt, rreg, wreg, escape}
+function write_zero(paddr, width) = {
+ let res : MemoryOpResult(bool) = mem_write_value(paddr, 8, to_bits(64, 0), false, false, false);
+ match (res) {
+ MemValue(true) => {
+ if(unsigned(width) > 8) then
+ write_zero(paddr + 8, width - 8)
Use a loop when you want a loop
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> +mapping clause encdec = RISCV_CBO(cbop, rs1)
+ <-> encdec_cbop(cbop) @ rs1 @ 0b010 @ 0b00000 @ 0b0001111
+
+mapping cbo_mnemonic : cbop <-> string = {
+ CBO_CLEAN <-> "cbo.clean",
+ CBO_FLUSH <-> "cbo.flush",
+ CBO_INVAL <-> "cbo.inval",
+ CBO_ZERO <-> "cbo.zero"
+}
+
+mapping clause assembly = RISCV_CBO(cbop, rs1)
+ <-> cbo_mnemonic(cbop) ^ spc() ^ reg_name(rs1)
+
+val write_zero: (xlenbits, xlenbits) -> MemoryOpResult(bool) effect {wmv, wmvt, rreg, wreg, escape}
+function write_zero(paddr, width) = {
+ let res : MemoryOpResult(bool) = mem_write_value(paddr, 8, to_bits(64, 0), false, false, false);
Why 8? Either do byte by byte or do max_mem_access at a time (which is
16), but don't hard-code an arbitrary word size using magic constants.
Also use zeros() rather than to_bits(N, 0).
Finally, this is broken if width isn't divisible by 8 (or whatever word
size is used), so there should be an assertion to ensure that never happens
if it's not expected to (i.e., since everything's a power of two, that it's
impossible to configure the cache block size as less than the word size),
or it should be handled gracefully (which is one reason to make the model
simple and just do a byte-by-byte loop).
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> +mapping cbo_mnemonic : cbop <-> string = {
+ CBO_CLEAN <-> "cbo.clean",
+ CBO_FLUSH <-> "cbo.flush",
+ CBO_INVAL <-> "cbo.inval",
+ CBO_ZERO <-> "cbo.zero"
+}
+
+mapping clause assembly = RISCV_CBO(cbop, rs1)
+ <-> cbo_mnemonic(cbop) ^ spc() ^ reg_name(rs1)
+
+val write_zero: (xlenbits, xlenbits) -> MemoryOpResult(bool) effect {wmv, wmvt, rreg, wreg, escape}
+function write_zero(paddr, width) = {
+ let res : MemoryOpResult(bool) = mem_write_value(paddr, 8, to_bits(64, 0), false, false, false);
+ match (res) {
+ MemValue(true) => {
+ if(unsigned(width) > 8) then
Spaces after if, and no parens needed
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> + let res : MemoryOpResult(bool) = mem_write_value(paddr, 8, to_bits(64, 0), false, false, false);
+ match (res) {
+ MemValue(true) => {
+ if(unsigned(width) > 8) then
+ write_zero(paddr + 8, width - 8)
+ else
+ MemValue(true)
+ },
+ MemValue(false) => MemValue(false),
+ MemException(e) => MemException(e)
+ }
+}
+
+val process_cbo_zero : (xlenbits, xlenbits) -> Retired effect {eamem, escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
+function process_cbo_zero(vaddr, width) = {
+ match ext_data_get_addr(to_bits(5, 0), vaddr, Write(Data), BYTE) {
The first argument should be rs1 for the instruction, and you have a bunch
of the same bug so I'm only commenting on this one.
And BYTE is definitely wrong, it needs to match the exact size of the
write you're performing, you can't be lazy like with paging and probe a
single byte when writing a whole page, it has to be exact.
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> + }
+}
+
+val process_cbo_zero : (xlenbits, xlenbits) -> Retired effect {eamem, escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
+function process_cbo_zero(vaddr, width) = {
+ match ext_data_get_addr(to_bits(5, 0), vaddr, Write(Data), BYTE) {
+ Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
+ Ext_DataAddr_OK(vaddr) =>
+ match translateAddr(vaddr, Write(Data)) {
+ TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+ TR_Address(paddr, _) => {
+ let eares : MemoryOpResult(unit) = mem_write_ea(paddr, 1, false, false, false);
+ match (eares) {
+ MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+ MemValue(_) => {
+ let res : MemoryOpResult(bool) = write_zero(paddr, width);
What if the block size is high enough that it covers multiple pages?
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> + MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+ MemValue(_) => {
+ let res : MemoryOpResult(bool) = write_zero(paddr, width);
+ match (res) {
+ MemValue(true) => RETIRE_SUCCESS,
+ MemValue(false) => internal_error("store got false from mem_write_value"),
+ MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
+ }
+ }
+ }
+ }
+ }
+ }
+}
+
+union translation_check = {
So... option(ExceptionType)
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> + match translateAddr(vaddr, Execute()) {
+ TR_Failure(e, _) => TransTrap(e),
+ TR_Address(paddr, _) => TransSuccess()
+ }
+ };
+ match fetch {
+ TransSuccess() => RETIRE_SUCCESS,
+ TransTrap(fe) =>
+ match (le, se, fe) {
+ (E_Load_Access_Fault(), _, _) => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL },
+ (_, E_SAMO_Access_Fault(), _) => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL },
+ (_, _, E_Fetch_Access_Fault()) => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL },
+ (E_Load_Page_Fault(), _, _) => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL },
+ (_, E_SAMO_Page_Fault(), _) => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL },
+ (_, _, E_Fetch_Page_Fault()) => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL },
+ (E_Extension(e), _ , _ ) => { ext_handle_data_check_error(e); RETIRE_FAIL }
Don't put spaces before commas like that
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> + }
+ }
+ }
+ }
+ }
+}
+
+union translation_check = {
+ TransTrap : ExceptionType,
+ TransSuccess : unit
+}
+
+val process_clean_inval : (xlenbits, xlenbits, bool, bool) -> Retired effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
+function process_clean_inval(vaddr, width, clean, inval) = {
+ let load: translation_check = match ext_data_get_addr(to_bits(5, 0), vaddr, Read(Data), BYTE) {
+ Ext_DataAddr_Error(e) => TransTrap(E_Reserved_14()),
What are all these uses of exception 14 for? You need to pass the
ext_data_addr_error to ext_handle_data_check_error and return RETIRE_FAIL
if you get an Ext_DataAddr_Error that you decide to honour, not some random
reserved exception cause.
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> + (_, E_SAMO_Access_Fault(), _) => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL },
+ (_, _, E_Fetch_Access_Fault()) => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL },
+ (E_Load_Page_Fault(), _, _) => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL },
+ (_, E_SAMO_Page_Fault(), _) => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL },
+ (_, _, E_Fetch_Page_Fault()) => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL },
+ (E_Extension(e), _ , _ ) => { ext_handle_data_check_error(e); RETIRE_FAIL }
+ }
+ }
+ }
+ }
+ }
+ }
+}
+
+function check_clean_flush(p : Privilege) -> bool = {
+ let ret : bool = ~(((p != Machine) & (menvcfg.CBCFE() == 0b0)) |
This variable is pointless
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> + if bit0 then EXTZ(0b0)
+ else if bit1 then EXTZ(0b1)
Just put the second bit in and avoid the EXTZ
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> +}
+
+function check_clean_flush(p : Privilege) -> bool = {
+ let ret : bool = ~(((p != Machine) & (menvcfg.CBCFE() == 0b0)) |
+ ((p == User) & (senvcfg.CBCFE() == 0b0)));
+ ret
+}
+
+function check_inval(p : Privilege) -> bits(2) = {
+ let bit0 : bool = ((p != Machine) & (menvcfg.CBIE() == 0b00)) |
+ ((p == User) & (senvcfg.CBIE() == 0b00));
+ let bit1 : bool = ((p != Machine) & (menvcfg.CBIE() == 0b01)) |
+ ((p == User) & (senvcfg.CBIE() == 0b01));
+ if bit0 then EXTZ(0b0)
+ else if bit1 then EXTZ(0b1)
+ else EXTZ(0b11)
EXTZ is a no-op
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> + let bit0 : bool = ((p != Machine) & (menvcfg.CBIE() == 0b00)) |
+ ((p == User) & (senvcfg.CBIE() == 0b00));
+ let bit1 : bool = ((p != Machine) & (menvcfg.CBIE() == 0b01)) |
+ ((p == User) & (senvcfg.CBIE() == 0b01));
Give the variables descriptive names, e.g. trap and flush
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> + (E_Load_Access_Fault(), _, _) => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL },
+ (_, E_SAMO_Access_Fault(), _) => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL },
+ (_, _, E_Fetch_Access_Fault()) => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL },
+ (E_Load_Page_Fault(), _, _) => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL },
+ (_, E_SAMO_Page_Fault(), _) => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL },
+ (_, _, E_Fetch_Page_Fault()) => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL },
+ (E_Extension(e), _ , _ ) => { ext_handle_data_check_error(e); RETIRE_FAIL }
+ }
+ }
+ }
+ }
+ }
+ }
+}
+
+function check_clean_flush(p : Privilege) -> bool = {
These names should probably be more obviously scoped to cache operations
and more clearly state that they're about "what operation is this
instruction mapped to"; check_foo sounds like an assertion
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> + }
+ }
+ }
+ }
+ }
+ }
+}
+
+function check_clean_flush(p : Privilege) -> bool = {
+ let ret : bool = ~(((p != Machine) & (menvcfg.CBCFE() == 0b0)) |
+ ((p == User) & (senvcfg.CBCFE() == 0b0)));
+ ret
+}
+
+function check_inval(p : Privilege) -> bits(2) = {
+ let bit0 : bool = ((p != Machine) & (menvcfg.CBIE() == 0b00)) |
Types shouldn't be needed
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> + let bit1 : bool = ((p != Machine) & (menvcfg.CBIE() == 0b01)) |
+ ((p == User) & (senvcfg.CBIE() == 0b01));
+ if bit0 then EXTZ(0b0)
+ else if bit1 then EXTZ(0b1)
+ else EXTZ(0b11)
+}
+
+function check_zero(p : Privilege) -> bool = {
+ let ret : bool = ~(((p != Machine) & (menvcfg.CBZE() == 0b0)) |
+ ((p == User) & (senvcfg.CBZE() == 0b0)));
+ ret
+}
+
+function clause execute(RISCV_CBO(cbop, rs1)) = {
+ let rs1_val = X(rs1);
+ let cache_block_size : xlenbits = plat_cache_block_size() ;
No random spaces
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> +}
+
+function check_zero(p : Privilege) -> bool = {
+ let ret : bool = ~(((p != Machine) & (menvcfg.CBZE() == 0b0)) |
+ ((p == User) & (senvcfg.CBZE() == 0b0)));
+ ret
+}
+
+function clause execute(RISCV_CBO(cbop, rs1)) = {
+ let rs1_val = X(rs1);
+ let cache_block_size : xlenbits = plat_cache_block_size() ;
+ let vaddr: xlenbits = rs1_val & ~(cache_block_size - EXTZ(0b1));
+ match cbop {
+ CBO_CLEAN => {
+ if (check_clean_flush(cur_privilege)) then
+ /* perform clean*/
Space before the *, but also, this comment is a waste of time
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> + if bit0 then EXTZ(0b0)
+ else if bit1 then EXTZ(0b1)
+ else EXTZ(0b11)
+}
+
+function check_zero(p : Privilege) -> bool = {
+ let ret : bool = ~(((p != Machine) & (menvcfg.CBZE() == 0b0)) |
+ ((p == User) & (senvcfg.CBZE() == 0b0)));
+ ret
+}
+
+function clause execute(RISCV_CBO(cbop, rs1)) = {
+ let rs1_val = X(rs1);
+ let cache_block_size : xlenbits = plat_cache_block_size() ;
+ let vaddr: xlenbits = rs1_val & ~(cache_block_size - EXTZ(0b1));
+ match cbop {
This seems like it'd be nicer as two steps:
1. Take the instruction's operation and map it to option(operation)
based on the CSRs
2. Treat that operation as the actual operation to perform (with
None() being handle_illegal)
Also avoids all the magic constants being returned from functions and
read here (I realise it's repurposing the encodings of the CSRs, but that's
not the most friendly way of writing it)
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> +}
+
+mapping clause encdec = RISCV_PREFETCH(op, rs1, offset)
+ <-> offset @ encdec_prefetch(op) @ rs1 @ 0b110 @ 0b00000 @ 0b0010011
+
+mapping pre_mnemonic : preop <-> string = {
+ PREFETCH_I <-> "prefetch.i",
+ PREFETCH_R <-> "prefetch.r",
+ PREFETCH_W <-> "prefetch.w"
+}
+
+mapping clause assembly = RISCV_PREFETCH(op, rs1, offset)
+ <-> pre_mnemonic(op) ^ spc() ^ hex_bits_12(offset @ 0b00000) ^ "(" ^ reg_name(rs1) ^ ")"
+
+function clause execute(RISCV_PREFETCH(preop, rs1, offset)) = {
+ /* do nothing other than translate_address for prefetch.i/r/w */
Why do we even bother doing that? They're just hints, they can be entirely
nop'ed out in the model like any other hint. Which is already the case,
given they're ORI instructions, and base.sail gets included before
cmoext.sail so the real ORIs will take precedence and this code is entirely
dead.
Especially since this is actually wrong, due to translateAddr having the
side-effect of (if enabled instead of trapping for software emulation)
atomically updating accessed and dirty bits as needed, which is
specifically not performed for prefetch.
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> + TR_Address(paddr, _) => RETIRE_SUCCESS
+ }
+ }
+ },
+ PREFETCH_R => {
+ match ext_data_get_addr(rs1, EXTS(offset @ 0b00000), Read(Data), BYTE) {
+ Ext_DataAddr_Error(e) => RETIRE_SUCCESS,
+ Ext_DataAddr_OK(vaddr) =>
+ match translateAddr(vaddr, Read(Data)) {
+ TR_Failure(e, _) => RETIRE_SUCCESS,
+ TR_Address(paddr, _) => RETIRE_SUCCESS
+ }
+ }
+ }
+ }
+}
Make sure every line has a terminating newline character (required by
POSIX for a file to be a valid text file)
------------------------------
In model/riscv_sys_control.sail
<#137 (comment)>:
> @@ -89,6 +89,7 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool =
0x304 => p == Machine, // mie
0x305 => p == Machine, // mtvec
0x306 => p == Machine & haveUsrMode(), // mcounteren
+ 0x30a => p == Machine, //menvcfg
Space after the //
------------------------------
In model/riscv_sys_regs.sail
<#137 (comment)>:
> @@ -813,3 +813,18 @@ function read_seed_csr() -> xlenbits = {
/* Writes to the seed CSR are ignored */
function write_seed_csr () -> option(xlenbits) = None()
+
+bitfield Envcfg : xlenbits = {
+ CBZE : 7,
+ CBCFE : 6,
+ CBIE : 5 .. 4
+}
+register senvcfg : Envcfg
+register menvcfg : Envcfg
+
+function legalize_envcfg(c : Envcfg, v : xlenbits) -> Envcfg = {
+ let c = update_CBZE(c, [v[7]]);
+ let c = update_CBCFE(c, [v[6]]);
+ let c = update_CBIE(c, v[5 .. 4]);
Doesn't this need to legalise 10?
------------------------------
In model/riscv_types.sail
<#137 (comment)>:
> +enum cbop = {CBO_CLEAN, CBO_FLUSH, CBO_INVAL, CBO_ZERO} /* cbo ops*/
+enum preop = {PREFETCH_I, PREFETCH_R, PREFETCH_W} /* prefetch ops*/
Follow the convention below; put them in a separate block and include the
extension names
------------------------------
In ocaml_emulator/platform_impl.ml
<#137 (comment)>:
> @@ -57,6 +57,8 @@ let rom_base = 0x00001000L;; (* Spike::DEFAULT_RSTVEC *)
let dram_size_ref = ref (Int64.(shift_left 64L 20))
+let cache_block_size_ref = ref (Int64.(64L))
Ok so this one defaults to 64 as I'd expect, unlike the C model
------------------------------
In c_emulator/riscv_sim.c
<#137 (comment)>:
> @@ -337,6 +340,16 @@ char *process_args(int argc, char **argv)
sailcov_file = strdup(optarg);
break;
#endif
+ case 'B':
+ block_size = atol(optarg);
+ if (((block_size & 7) == 0) && (block_size < 4096)) {
I can't obviously find either of these restrictions in the spec; where
have these come from? 4096 seems pretty unproblematic, that's a whole page,
things just get awkward when you cover multiple pages, but the PMP already
makes that an issue.
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> + }
+ }
+ }
+}
+
+union translation_check = {
+ TransTrap : ExceptionType,
+ TransSuccess : unit
+}
+
+val process_clean_inval : (xlenbits, xlenbits, bool, bool) -> Retired effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
+function process_clean_inval(vaddr, width, clean, inval) = {
+ let load: translation_check = match ext_data_get_addr(to_bits(5, 0), vaddr, Read(Data), BYTE) {
+ Ext_DataAddr_Error(e) => TransTrap(E_Reserved_14()),
+ Ext_DataAddr_OK(vaddr) =>
+ match translateAddr(vaddr, Read(Data)) {
How does invalidate interact with the dirty bit of page table entries?
Just translating a read won't dirty the page, but surely an invalidate
needs to dirty the page if actually invalidating rather than just
cleaning/flushing? Though whether it's "only dirty if the cache line is
dirty" or "always dirty even if there's nothing to write back" I don't
know. I can only see discussion of accessed and dirty bits for prefetch and
zeroing, not management instruction.
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> + }
+ }
+ }
+}
+
+union translation_check = {
+ TransTrap : ExceptionType,
+ TransSuccess : unit
+}
+
+val process_clean_inval : (xlenbits, xlenbits, bool, bool) -> Retired effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
+function process_clean_inval(vaddr, width, clean, inval) = {
+ let load: translation_check = match ext_data_get_addr(to_bits(5, 0), vaddr, Read(Data), BYTE) {
+ Ext_DataAddr_Error(e) => TransTrap(E_Reserved_14()),
+ Ext_DataAddr_OK(vaddr) =>
+ match translateAddr(vaddr, Read(Data)) {
(The answer to that affects whether or not you can clean this up by just
hoisting all three load, store and fetch calculations and matching on them
all at the same time, which would flatten this function somewhat)
—
Reply to this email directly, view it on GitHub
<#137 (review)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AHPXVJWIR7QEM5BHJMGYTKTURQR4HANCNFSM5KKGQEIA>
.
Triage notifications on the go with GitHub Mobile for iOS
<https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675>
or Android
<https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>.
You are receiving this because you are subscribed to this thread.Message
ID: ***@***.***>
|
|
I am concerned that jrtc27 has pointed out things that are bugs in the
code, yet there are no tests that cover those.
Shouldn't there be?
…On Fri, Dec 17, 2021 at 10:20 PM Jessica Clarke ***@***.***> wrote:
***@***.**** commented on this pull request.
Various initial feedback; generally only commented on the first instance
of something even when it applies multiple times, so please check for other
instances of things I've said, especially when it comes to code formatting
------------------------------
In Makefile
<#137 (comment)>:
> @@ -29,6 +29,7 @@ SAIL_DEFAULT_INST += riscv_insts_zbc.sail
SAIL_DEFAULT_INST += riscv_insts_zbs.sail
SAIL_DEFAULT_INST += riscv_insts_zkn.sail
SAIL_DEFAULT_INST += riscv_insts_zks.sail
+SAIL_DEFAULT_INST += riscv_insts_cmoext.sail
As you can see from the big block above, each Zfoo gets its own zfoo.sail
file, so Zicbom, Zicbop and Zicboz should get their own files named
accordingly
------------------------------
In c_emulator/riscv_platform_impl.c
<#137 (comment)>:
> @@ -20,6 +20,8 @@ uint64_t rv_ram_size = UINT64_C(0x4000000);
uint64_t rv_rom_base = UINT64_C(0x1000);
uint64_t rv_rom_size = UINT64_C(0x100);
+uint64_t rv_cache_block_size = UINT64_C(0x10);
16 bytes is a strange default, 64 seems like a more common cache line size
to default to
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> @@ -0,0 +1,245 @@
+/* ****************************************************************** */
+/* This file specifies the instructions in the cmo extension */
Not an extension name
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> @@ -0,0 +1,245 @@
+/* ****************************************************************** */
+/* This file specifies the instructions in the cmo extension */
+
+
+/* ****************************************************************** */
+union clause ast = RISCV_CBO : (cbop, regidx)
Should be specific to Zcbop
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> @@ -0,0 +1,245 @@
+/* ****************************************************************** */
+/* This file specifies the instructions in the cmo extension */
+
+
+/* ****************************************************************** */
+union clause ast = RISCV_CBO : (cbop, regidx)
+
+mapping encdec_cbop : cbop <-> bits(12) = {
+ CBO_CLEAN <-> 0b000000000001,
+ CBO_FLUSH <-> 0b000000000010,
+ CBO_INVAL <-> 0b000000000000,
+ CBO_ZERO <-> 0b000000000100
CBO_ZERO is part of a separate extension to the other three so should get
its own ast clause
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> @@ -0,0 +1,245 @@
+/* ****************************************************************** */
+/* This file specifies the instructions in the cmo extension */
+
+
+/* ****************************************************************** */
+union clause ast = RISCV_CBO : (cbop, regidx)
+
+mapping encdec_cbop : cbop <-> bits(12) = {
+ CBO_CLEAN <-> 0b000000000001,
+ CBO_FLUSH <-> 0b000000000010,
+ CBO_INVAL <-> 0b000000000000,
+ CBO_ZERO <-> 0b000000000100
+}
+
+mapping clause encdec = RISCV_CBO(cbop, rs1)
These need guards on the extensions being enabled
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> + CBO_CLEAN <-> "cbo.clean",
+ CBO_FLUSH <-> "cbo.flush",
+ CBO_INVAL <-> "cbo.inval",
+ CBO_ZERO <-> "cbo.zero"
+}
+
+mapping clause assembly = RISCV_CBO(cbop, rs1)
+ <-> cbo_mnemonic(cbop) ^ spc() ^ reg_name(rs1)
+
+val write_zero: (xlenbits, xlenbits) -> MemoryOpResult(bool) effect {wmv, wmvt, rreg, wreg, escape}
+function write_zero(paddr, width) = {
+ let res : MemoryOpResult(bool) = mem_write_value(paddr, 8, to_bits(64, 0), false, false, false);
+ match (res) {
+ MemValue(true) => {
+ if(unsigned(width) > 8) then
+ write_zero(paddr + 8, width - 8)
Use a loop when you want a loop
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> +mapping clause encdec = RISCV_CBO(cbop, rs1)
+ <-> encdec_cbop(cbop) @ rs1 @ 0b010 @ 0b00000 @ 0b0001111
+
+mapping cbo_mnemonic : cbop <-> string = {
+ CBO_CLEAN <-> "cbo.clean",
+ CBO_FLUSH <-> "cbo.flush",
+ CBO_INVAL <-> "cbo.inval",
+ CBO_ZERO <-> "cbo.zero"
+}
+
+mapping clause assembly = RISCV_CBO(cbop, rs1)
+ <-> cbo_mnemonic(cbop) ^ spc() ^ reg_name(rs1)
+
+val write_zero: (xlenbits, xlenbits) -> MemoryOpResult(bool) effect {wmv, wmvt, rreg, wreg, escape}
+function write_zero(paddr, width) = {
+ let res : MemoryOpResult(bool) = mem_write_value(paddr, 8, to_bits(64, 0), false, false, false);
Why 8? Either do byte by byte or do max_mem_access at a time (which is
16), but don't hard-code an arbitrary word size using magic constants.
Also use zeros() rather than to_bits(N, 0).
Finally, this is broken if width isn't divisible by 8 (or whatever word
size is used), so there should be an assertion to ensure that never happens
if it's not expected to (i.e., since everything's a power of two, that it's
impossible to configure the cache block size as less than the word size),
or it should be handled gracefully (which is one reason to make the model
simple and just do a byte-by-byte loop).
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> +mapping cbo_mnemonic : cbop <-> string = {
+ CBO_CLEAN <-> "cbo.clean",
+ CBO_FLUSH <-> "cbo.flush",
+ CBO_INVAL <-> "cbo.inval",
+ CBO_ZERO <-> "cbo.zero"
+}
+
+mapping clause assembly = RISCV_CBO(cbop, rs1)
+ <-> cbo_mnemonic(cbop) ^ spc() ^ reg_name(rs1)
+
+val write_zero: (xlenbits, xlenbits) -> MemoryOpResult(bool) effect {wmv, wmvt, rreg, wreg, escape}
+function write_zero(paddr, width) = {
+ let res : MemoryOpResult(bool) = mem_write_value(paddr, 8, to_bits(64, 0), false, false, false);
+ match (res) {
+ MemValue(true) => {
+ if(unsigned(width) > 8) then
Spaces after if, and no parens needed
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> + let res : MemoryOpResult(bool) = mem_write_value(paddr, 8, to_bits(64, 0), false, false, false);
+ match (res) {
+ MemValue(true) => {
+ if(unsigned(width) > 8) then
+ write_zero(paddr + 8, width - 8)
+ else
+ MemValue(true)
+ },
+ MemValue(false) => MemValue(false),
+ MemException(e) => MemException(e)
+ }
+}
+
+val process_cbo_zero : (xlenbits, xlenbits) -> Retired effect {eamem, escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
+function process_cbo_zero(vaddr, width) = {
+ match ext_data_get_addr(to_bits(5, 0), vaddr, Write(Data), BYTE) {
The first argument should be rs1 for the instruction, and you have a bunch
of the same bug so I'm only commenting on this one.
And BYTE is definitely wrong, it needs to match the exact size of the
write you're performing, you can't be lazy like with paging and probe a
single byte when writing a whole page, it has to be exact.
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> + }
+}
+
+val process_cbo_zero : (xlenbits, xlenbits) -> Retired effect {eamem, escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
+function process_cbo_zero(vaddr, width) = {
+ match ext_data_get_addr(to_bits(5, 0), vaddr, Write(Data), BYTE) {
+ Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
+ Ext_DataAddr_OK(vaddr) =>
+ match translateAddr(vaddr, Write(Data)) {
+ TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+ TR_Address(paddr, _) => {
+ let eares : MemoryOpResult(unit) = mem_write_ea(paddr, 1, false, false, false);
+ match (eares) {
+ MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+ MemValue(_) => {
+ let res : MemoryOpResult(bool) = write_zero(paddr, width);
What if the block size is high enough that it covers multiple pages?
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> + MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+ MemValue(_) => {
+ let res : MemoryOpResult(bool) = write_zero(paddr, width);
+ match (res) {
+ MemValue(true) => RETIRE_SUCCESS,
+ MemValue(false) => internal_error("store got false from mem_write_value"),
+ MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
+ }
+ }
+ }
+ }
+ }
+ }
+}
+
+union translation_check = {
So... option(ExceptionType)
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> + match translateAddr(vaddr, Execute()) {
+ TR_Failure(e, _) => TransTrap(e),
+ TR_Address(paddr, _) => TransSuccess()
+ }
+ };
+ match fetch {
+ TransSuccess() => RETIRE_SUCCESS,
+ TransTrap(fe) =>
+ match (le, se, fe) {
+ (E_Load_Access_Fault(), _, _) => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL },
+ (_, E_SAMO_Access_Fault(), _) => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL },
+ (_, _, E_Fetch_Access_Fault()) => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL },
+ (E_Load_Page_Fault(), _, _) => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL },
+ (_, E_SAMO_Page_Fault(), _) => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL },
+ (_, _, E_Fetch_Page_Fault()) => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL },
+ (E_Extension(e), _ , _ ) => { ext_handle_data_check_error(e); RETIRE_FAIL }
Don't put spaces before commas like that
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> + }
+ }
+ }
+ }
+ }
+}
+
+union translation_check = {
+ TransTrap : ExceptionType,
+ TransSuccess : unit
+}
+
+val process_clean_inval : (xlenbits, xlenbits, bool, bool) -> Retired effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
+function process_clean_inval(vaddr, width, clean, inval) = {
+ let load: translation_check = match ext_data_get_addr(to_bits(5, 0), vaddr, Read(Data), BYTE) {
+ Ext_DataAddr_Error(e) => TransTrap(E_Reserved_14()),
What are all these uses of exception 14 for? You need to pass the
ext_data_addr_error to ext_handle_data_check_error and return RETIRE_FAIL
if you get an Ext_DataAddr_Error that you decide to honour, not some random
reserved exception cause.
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> + (_, E_SAMO_Access_Fault(), _) => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL },
+ (_, _, E_Fetch_Access_Fault()) => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL },
+ (E_Load_Page_Fault(), _, _) => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL },
+ (_, E_SAMO_Page_Fault(), _) => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL },
+ (_, _, E_Fetch_Page_Fault()) => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL },
+ (E_Extension(e), _ , _ ) => { ext_handle_data_check_error(e); RETIRE_FAIL }
+ }
+ }
+ }
+ }
+ }
+ }
+}
+
+function check_clean_flush(p : Privilege) -> bool = {
+ let ret : bool = ~(((p != Machine) & (menvcfg.CBCFE() == 0b0)) |
This variable is pointless
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> + if bit0 then EXTZ(0b0)
+ else if bit1 then EXTZ(0b1)
Just put the second bit in and avoid the EXTZ
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> +}
+
+function check_clean_flush(p : Privilege) -> bool = {
+ let ret : bool = ~(((p != Machine) & (menvcfg.CBCFE() == 0b0)) |
+ ((p == User) & (senvcfg.CBCFE() == 0b0)));
+ ret
+}
+
+function check_inval(p : Privilege) -> bits(2) = {
+ let bit0 : bool = ((p != Machine) & (menvcfg.CBIE() == 0b00)) |
+ ((p == User) & (senvcfg.CBIE() == 0b00));
+ let bit1 : bool = ((p != Machine) & (menvcfg.CBIE() == 0b01)) |
+ ((p == User) & (senvcfg.CBIE() == 0b01));
+ if bit0 then EXTZ(0b0)
+ else if bit1 then EXTZ(0b1)
+ else EXTZ(0b11)
EXTZ is a no-op
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> + let bit0 : bool = ((p != Machine) & (menvcfg.CBIE() == 0b00)) |
+ ((p == User) & (senvcfg.CBIE() == 0b00));
+ let bit1 : bool = ((p != Machine) & (menvcfg.CBIE() == 0b01)) |
+ ((p == User) & (senvcfg.CBIE() == 0b01));
Give the variables descriptive names, e.g. trap and flush
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> + (E_Load_Access_Fault(), _, _) => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL },
+ (_, E_SAMO_Access_Fault(), _) => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL },
+ (_, _, E_Fetch_Access_Fault()) => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL },
+ (E_Load_Page_Fault(), _, _) => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL },
+ (_, E_SAMO_Page_Fault(), _) => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL },
+ (_, _, E_Fetch_Page_Fault()) => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL },
+ (E_Extension(e), _ , _ ) => { ext_handle_data_check_error(e); RETIRE_FAIL }
+ }
+ }
+ }
+ }
+ }
+ }
+}
+
+function check_clean_flush(p : Privilege) -> bool = {
These names should probably be more obviously scoped to cache operations
and more clearly state that they're about "what operation is this
instruction mapped to"; check_foo sounds like an assertion
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> + }
+ }
+ }
+ }
+ }
+ }
+}
+
+function check_clean_flush(p : Privilege) -> bool = {
+ let ret : bool = ~(((p != Machine) & (menvcfg.CBCFE() == 0b0)) |
+ ((p == User) & (senvcfg.CBCFE() == 0b0)));
+ ret
+}
+
+function check_inval(p : Privilege) -> bits(2) = {
+ let bit0 : bool = ((p != Machine) & (menvcfg.CBIE() == 0b00)) |
Types shouldn't be needed
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> + let bit1 : bool = ((p != Machine) & (menvcfg.CBIE() == 0b01)) |
+ ((p == User) & (senvcfg.CBIE() == 0b01));
+ if bit0 then EXTZ(0b0)
+ else if bit1 then EXTZ(0b1)
+ else EXTZ(0b11)
+}
+
+function check_zero(p : Privilege) -> bool = {
+ let ret : bool = ~(((p != Machine) & (menvcfg.CBZE() == 0b0)) |
+ ((p == User) & (senvcfg.CBZE() == 0b0)));
+ ret
+}
+
+function clause execute(RISCV_CBO(cbop, rs1)) = {
+ let rs1_val = X(rs1);
+ let cache_block_size : xlenbits = plat_cache_block_size() ;
No random spaces
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> +}
+
+function check_zero(p : Privilege) -> bool = {
+ let ret : bool = ~(((p != Machine) & (menvcfg.CBZE() == 0b0)) |
+ ((p == User) & (senvcfg.CBZE() == 0b0)));
+ ret
+}
+
+function clause execute(RISCV_CBO(cbop, rs1)) = {
+ let rs1_val = X(rs1);
+ let cache_block_size : xlenbits = plat_cache_block_size() ;
+ let vaddr: xlenbits = rs1_val & ~(cache_block_size - EXTZ(0b1));
+ match cbop {
+ CBO_CLEAN => {
+ if (check_clean_flush(cur_privilege)) then
+ /* perform clean*/
Space before the *, but also, this comment is a waste of time
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> + if bit0 then EXTZ(0b0)
+ else if bit1 then EXTZ(0b1)
+ else EXTZ(0b11)
+}
+
+function check_zero(p : Privilege) -> bool = {
+ let ret : bool = ~(((p != Machine) & (menvcfg.CBZE() == 0b0)) |
+ ((p == User) & (senvcfg.CBZE() == 0b0)));
+ ret
+}
+
+function clause execute(RISCV_CBO(cbop, rs1)) = {
+ let rs1_val = X(rs1);
+ let cache_block_size : xlenbits = plat_cache_block_size() ;
+ let vaddr: xlenbits = rs1_val & ~(cache_block_size - EXTZ(0b1));
+ match cbop {
This seems like it'd be nicer as two steps:
1. Take the instruction's operation and map it to option(operation)
based on the CSRs
2. Treat that operation as the actual operation to perform (with
None() being handle_illegal)
Also avoids all the magic constants being returned from functions and
read here (I realise it's repurposing the encodings of the CSRs, but that's
not the most friendly way of writing it)
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> +}
+
+mapping clause encdec = RISCV_PREFETCH(op, rs1, offset)
+ <-> offset @ encdec_prefetch(op) @ rs1 @ 0b110 @ 0b00000 @ 0b0010011
+
+mapping pre_mnemonic : preop <-> string = {
+ PREFETCH_I <-> "prefetch.i",
+ PREFETCH_R <-> "prefetch.r",
+ PREFETCH_W <-> "prefetch.w"
+}
+
+mapping clause assembly = RISCV_PREFETCH(op, rs1, offset)
+ <-> pre_mnemonic(op) ^ spc() ^ hex_bits_12(offset @ 0b00000) ^ "(" ^ reg_name(rs1) ^ ")"
+
+function clause execute(RISCV_PREFETCH(preop, rs1, offset)) = {
+ /* do nothing other than translate_address for prefetch.i/r/w */
Why do we even bother doing that? They're just hints, they can be entirely
nop'ed out in the model like any other hint. Which is already the case,
given they're ORI instructions, and base.sail gets included before
cmoext.sail so the real ORIs will take precedence and this code is entirely
dead.
Especially since this is actually wrong, due to translateAddr having the
side-effect of (if enabled instead of trapping for software emulation)
atomically updating accessed and dirty bits as needed, which is
specifically not performed for prefetch.
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> + TR_Address(paddr, _) => RETIRE_SUCCESS
+ }
+ }
+ },
+ PREFETCH_R => {
+ match ext_data_get_addr(rs1, EXTS(offset @ 0b00000), Read(Data), BYTE) {
+ Ext_DataAddr_Error(e) => RETIRE_SUCCESS,
+ Ext_DataAddr_OK(vaddr) =>
+ match translateAddr(vaddr, Read(Data)) {
+ TR_Failure(e, _) => RETIRE_SUCCESS,
+ TR_Address(paddr, _) => RETIRE_SUCCESS
+ }
+ }
+ }
+ }
+}
Make sure every line has a terminating newline character (required by
POSIX for a file to be a valid text file)
------------------------------
In model/riscv_sys_control.sail
<#137 (comment)>:
> @@ -89,6 +89,7 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool =
0x304 => p == Machine, // mie
0x305 => p == Machine, // mtvec
0x306 => p == Machine & haveUsrMode(), // mcounteren
+ 0x30a => p == Machine, //menvcfg
Space after the //
------------------------------
In model/riscv_sys_regs.sail
<#137 (comment)>:
> @@ -813,3 +813,18 @@ function read_seed_csr() -> xlenbits = {
/* Writes to the seed CSR are ignored */
function write_seed_csr () -> option(xlenbits) = None()
+
+bitfield Envcfg : xlenbits = {
+ CBZE : 7,
+ CBCFE : 6,
+ CBIE : 5 .. 4
+}
+register senvcfg : Envcfg
+register menvcfg : Envcfg
+
+function legalize_envcfg(c : Envcfg, v : xlenbits) -> Envcfg = {
+ let c = update_CBZE(c, [v[7]]);
+ let c = update_CBCFE(c, [v[6]]);
+ let c = update_CBIE(c, v[5 .. 4]);
Doesn't this need to legalise 10?
------------------------------
In model/riscv_types.sail
<#137 (comment)>:
> +enum cbop = {CBO_CLEAN, CBO_FLUSH, CBO_INVAL, CBO_ZERO} /* cbo ops*/
+enum preop = {PREFETCH_I, PREFETCH_R, PREFETCH_W} /* prefetch ops*/
Follow the convention below; put them in a separate block and include the
extension names
------------------------------
In ocaml_emulator/platform_impl.ml
<#137 (comment)>:
> @@ -57,6 +57,8 @@ let rom_base = 0x00001000L;; (* Spike::DEFAULT_RSTVEC *)
let dram_size_ref = ref (Int64.(shift_left 64L 20))
+let cache_block_size_ref = ref (Int64.(64L))
Ok so this one defaults to 64 as I'd expect, unlike the C model
------------------------------
In c_emulator/riscv_sim.c
<#137 (comment)>:
> @@ -337,6 +340,16 @@ char *process_args(int argc, char **argv)
sailcov_file = strdup(optarg);
break;
#endif
+ case 'B':
+ block_size = atol(optarg);
+ if (((block_size & 7) == 0) && (block_size < 4096)) {
I can't obviously find either of these restrictions in the spec; where
have these come from? 4096 seems pretty unproblematic, that's a whole page,
things just get awkward when you cover multiple pages, but the PMP already
makes that an issue.
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> + }
+ }
+ }
+}
+
+union translation_check = {
+ TransTrap : ExceptionType,
+ TransSuccess : unit
+}
+
+val process_clean_inval : (xlenbits, xlenbits, bool, bool) -> Retired effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
+function process_clean_inval(vaddr, width, clean, inval) = {
+ let load: translation_check = match ext_data_get_addr(to_bits(5, 0), vaddr, Read(Data), BYTE) {
+ Ext_DataAddr_Error(e) => TransTrap(E_Reserved_14()),
+ Ext_DataAddr_OK(vaddr) =>
+ match translateAddr(vaddr, Read(Data)) {
How does invalidate interact with the dirty bit of page table entries?
Just translating a read won't dirty the page, but surely an invalidate
needs to dirty the page if actually invalidating rather than just
cleaning/flushing? Though whether it's "only dirty if the cache line is
dirty" or "always dirty even if there's nothing to write back" I don't
know. I can only see discussion of accessed and dirty bits for prefetch and
zeroing, not management instruction.
------------------------------
In model/riscv_insts_cmoext.sail
<#137 (comment)>:
> + }
+ }
+ }
+}
+
+union translation_check = {
+ TransTrap : ExceptionType,
+ TransSuccess : unit
+}
+
+val process_clean_inval : (xlenbits, xlenbits, bool, bool) -> Retired effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
+function process_clean_inval(vaddr, width, clean, inval) = {
+ let load: translation_check = match ext_data_get_addr(to_bits(5, 0), vaddr, Read(Data), BYTE) {
+ Ext_DataAddr_Error(e) => TransTrap(E_Reserved_14()),
+ Ext_DataAddr_OK(vaddr) =>
+ match translateAddr(vaddr, Read(Data)) {
(The answer to that affects whether or not you can clean this up by just
hoisting all three load, store and fetch calculations and matching on them
all at the same time, which would flatten this function somewhat)
—
Reply to this email directly, view it on GitHub
<#137 (review)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AHPXVJWIR7QEM5BHJMGYTKTURQR4HANCNFSM5KKGQEIA>
.
Triage notifications on the go with GitHub Mobile for iOS
<https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675>
or Android
<https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>.
You are receiving this because you are subscribed to this thread.Message
ID: ***@***.***>
|
Yes, that's right; I took an educated guess based on the low number of additional spaces that the intent was not to line things up |
liweiwei90
force-pushed
the
plct-cmo-upstream
branch
from
754e168 to
3e05453
Compare
liweiwei90
force-pushed
the
plct-cmo-upstream
branch
from
3e05453 to
f010116
Compare
|
What are the next steps to take here? |
jrtc27
reviewed
Jan 26, 2022
liweiwei90
force-pushed
the
plct-cmo-upstream
branch
from
f010116 to
54f4dc9
Compare
liweiwei90
force-pushed
the
plct-cmo-upstream
branch
from
71ccd49 to
e6c4131
Compare
arichardson
reviewed
Aug 24, 2022
liweiwei90
force-pushed
the
plct-cmo-upstream
branch
from
e6c4131 to
9440439
Compare
arichardson
reviewed
Jan 26, 2023
|
The description of this PR says prefetch is supported, but I don't see any Zicbop support in the code? Maybe that got lost while splitting up the files? |
|
What is the status on this PR? Given that the Zicbo[mpz] extensions are comparatively self-contained (and we don't have to implement any real cache-management functionality/prefetchers), I'd like to see this pushed over the finish line sooner than later. |
Yeah. the file with the support for Zicbop is deleted in previous updates. It will be dead code since prefetch instructions reuse the encoding of existed instruction. |
Sorry, I didn't maintain this PR after I replied the comments and update the code to fix the problems several month ago. I think most of the questions have been resolved or replied(may need further discussion).
Yeah. I agree. I'll try to re-maintain and update it sooner. |
liweiwei90
force-pushed
the
plct-cmo-upstream
branch
from
9440439 to
3337007
Compare
|
At a glance I don't think the extension hooks comments have been properly addressed |
Sorry. Do you mean ext_data_get_addr problem? |
Yes. You give it a register index for the base address register used, an offset from that register's value and the size of the memory operation being performed. All of those must be correct. Currently you pass zeros() as the register index, the virtual address as the offset and BYTE as the width. This works in the upstream Sail model because all it does is return |
Yeah. I don't find the original meaning of this function as I commented before. So I used it as an address calculation progress. |
We can change it to take the actual number of bytes rather than one of the width enum values. |
OK. I'll change it. |
|
Action items from today:
|
ptomsich
removed
the
tgmm-agenda
OK. I'll check the above comments again and mark them as resolved or update the patch if needed. The ACT PR can be found in riscv-non-isa/riscv-arch-test#226 |
liweiwei90
force-pushed
the
plct-cmo-upstream
branch
from
fabc698 to
ab52bc3
Compare
|
Two problems may need further discussion:
|
The specification does not disallow it, so it must be supported by our implementations. The only requirements (from the specification) are:
|
liweiwei90
force-pushed
the
plct-cmo-upstream
branch
from
ab52bc3 to
5a4b823
Compare
liweiwei90
force-pushed
the
plct-cmo-upstream
branch
from
5a4b823 to
2424492
Compare
(They will be overlapped by ORI instruciton).
liweiwei90
force-pushed
the
plct-cmo-upstream
branch
from
2424492 to
ebf25f6
Compare
Merged
Timmmm
reviewed
Nov 17, 2023
| @@ -127,7 +127,7 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = { | |||
| /* Get the address, X(rs1) (no offset). | |||
| * Extensions might perform additional checks on address validity. | |||
| */ | |||
| match ext_data_get_addr(rs1, zeros(), Read(Data), width) { | |||
| match ext_data_get_addr(rs1, zeros(), Read(Data), EXTZ(size_bits(width))) { | |||
There was a problem hiding this comment.
Shouldn't these size_bits be word_width_bytes everywhere?
Also when you rebase you'll have to upload a load of the vector code that calls ext_data_get_addr(). Though you can be lazy and just wait if you want, because I am rebasing/updating this...
Timmmm
reviewed
Nov 17, 2023
| @@ -116,7 +116,7 @@ type ext_data_addr_error = unit | |||
|
|
|||
| /* Default data addr is just base register + immediate offset (may be zero). | |||
| Extensions might override and add additional checks. */ | |||
| function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType(ext_access_type), width : word_width) | |||
| function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType(ext_access_type), width : xlenbits) | |||
There was a problem hiding this comment.
Is xlenbits the right type? Maybe nat would be better (or range(1, 1024) for performance reasons).
|
I'm working on this. There are a number of things I've noticed/changed - I'll list them here just so they don't get lost in case of unexpected bus accidents. But if you can wait a few weeks I will upload a PR.
|
|
As mentioned back in May, cbo.zero support in Sail is gating the ability to verify the cbo.zero tests that were recently added to riscv-arch-test. Looking forward to this PR being completed. |
|
Nudge. |
|
Coincidentally I prepared a PR today. Just getting approval to send it (shouldn't take long). |
|
@davidharrishmc See #455 |
|
#455 was merged so I'll close this one. Thanks for the initial code @liweiwei90! |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
add support for cmo extension: